i:Id, A:MsgA. @i: A  IdMsgA 

latex

Definitions	System, MsgA, @i: A, Unit, P  Q, P & Q, P  Q, a = b, , Prop, b, A, b, x:A. B(x), , t  T, Id
Lemmas	Id wf, ma-empty wf, assert wf, not wf, bnot wf, bool wf, eq id wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, msga wf, m-sys-at wf